/**
 * Heraclito
 * 
 * Copyright (C) 2011  João Carlos Gluz/Marcel Mossmann
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301,
 * USA.
 *
 */
package logic;

import java.io.Serializable;

public class Formula implements Serializable{
    public static final int
        PROPOSITION =      1,
        PARENTHESIS =      2,
        NEGATION =          3,
        CONJUNCTION =       4,
        DISJUNCTION =       5,
        CONDITIONAL =       6,
        BICONDITIONAL =     7,
        EXCLDISJUNCTION =   8;
    
    protected int type;
    protected String proposition;
    Formula left,right,next;

   public Formula() {
       type =0;
       proposition = null;
       left = null;
       right = null;
       next = null;
   }

   public Formula(int t, String p) {
       type =t;
       proposition = p;
       left = null;
       right = null;
       next = null;
   }
   public Formula(int t, Formula n) {
       type =t;
       next = n;
       proposition = null;
       left = null;
       right = null;
 }
   
   public Formula(int t, Formula l, Formula r) {
       type =t;
       left = l;
       right = r;
       proposition = null;
       next = null;
 }

  
    public int getType() {
        return type;
    }

    public void setType(int t) {
        type=t;
    }

    public String getProposition() {
        return proposition;
    }

    public void setProposition(String s) {
        proposition=s;
    }

    public Formula getLeft() {
        return left;
    }

    public void setLeft(Formula l) {
        left=l;
    }

    public Formula getRight() {
        return right;
    }

    public void setRight(Formula r) {
        right=r;
    }

    public Formula getNext() {
        return next;
    }

    public void setNext(Formula n) {
        next=n;
    }

    public String display () {
		
        if (type==PROPOSITION) {
            return proposition;
        } else if (type==NEGATION) {
            String n = next.display();
            if (next.getType()==PROPOSITION || next.getType()==PARENTHESIS || next.getType()==NEGATION) {
                return "~" + n;
            } else {
                return "~(" + n + ")";
            }
            
        } else if (type==PARENTHESIS) {
            String n = next.display();
            return "(" + n + ")";
        } else {
            String l = left.display();
            String r = right.display();
            switch(type) {
                case   CONJUNCTION:
                    if(left.getType()==DISJUNCTION||left.getType()==CONDITIONAL||left.getType()==BICONDITIONAL)
                        l="("+l+")";
                    if(right.getType()==DISJUNCTION||right.getType()==CONDITIONAL||right.getType()==BICONDITIONAL)
                        r="("+r+")";
                        return l + " ^ " + r;
                case   DISJUNCTION:
                    if(left.getType()==CONDITIONAL||left.getType()==BICONDITIONAL)
                        l="("+l+")";
                    if(right.getType()==CONDITIONAL||right.getType()==BICONDITIONAL)
                        r="("+r+")";
                        return l + " v " + r;
                case   EXCLDISJUNCTION:
                        return l + " * " + r;
                case   CONDITIONAL:
                    if(left.getType()==BICONDITIONAL)
                        l="("+l+")";
                    if(right.getType()==BICONDITIONAL)
                        r="("+r+")";
                        return l + " -> " + r;
                case   BICONDITIONAL:
                        return l + " <-> " + r;
            }
            return "";
            
        }
    }
        
     public boolean equalsTo(Formula f) {
        if (type==f.getType()) {
            
            if (type==PROPOSITION) 
                return proposition.equals(f.getProposition());
        
            if (type==NEGATION || type==PARENTHESIS)
                return next.equalsTo(f.getNext());
        
            if (left.equalsTo(f.getLeft()) )
                return right.equalsTo(f.getRight());
        } else if (type==PARENTHESIS) {
            return (next.equalsTo(f));
        } else if (f.getType()==PARENTHESIS) {
            return (this.equalsTo(f.getNext()));
        }
        
        return false;
    }
   		
    public void parse(String textFormula) throws ScannerException, ParserException {
         final Scanner scanner = new Scanner(textFormula);
         scanner.tokenize();
         scanner.reformat();
         final Parser parser = new Parser(scanner.getTokenStream());
         parser.parse(this);
         this.setProposition(display());
    }

}
